形式手法 検証アプローチ
検証アプローチは主に
がある。
プログラム検証というものもあるっぽい。定理証明を包括するものがプログラム検証というものになる。 定理証明$ \subset プログラム検証
アプローチ方法は以下がある
モデルベースアプローチ
代数アプローチ
プロセス代数
論理アプローチ
(RTL, TLA)
リアクティブアプローチ
(Petri-‐nets, SDL, SAO)
複合アプローチ
LOTOS(Act One + CCS)
参考
酒匂 寛. 成功した形式手法導入調査例の分析と発見. 2012/11/15.